Convert symbolic LTS using LDDs to a BDD based representation #66
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
There was a problem hiding this comment.
Pull request overview
This pull request converts symbolic LTS representation from LDDs to BDDs and begins implementing signature-based strong symbolic bisimulation. The PR also reorganizes third-party dependencies by moving pest_consume and mcrl2-sys to external GitHub repositories.
Changes:
- Adds BDD-based symbolic LTS representation and conversion from LDD format
- Implements initial signature refinement algorithm (incomplete)
- Moves third-party code (
pest_consume,mcrl2-sys) to separate repositories - Adds new CLI commands to
merc-symtool for symbolic LTS operations - Renames mCRL2 features for consistency
Reviewed changes
Copilot reviewed 58 out of 62 changed files in this pull request and generated 5 comments.
Show a summary per file
| File | Description |
|---|---|
| tools/sym/src/main.rs | Adds new CLI interface with commands for info, explore, reorder, convert, and reduce operations on symbolic LTS |
| crates/symbolic/src/symbolic_lts_bdd.rs | New module implementing BDD-based symbolic LTS representation with conversion from LDD format |
| crates/symbolic/src/sigref.rs | New module for signature refinement algorithm (incomplete implementation) |
| crates/symbolic/src/ldd_to_bdd.rs | Refactors LDD to BDD conversion to use explicit variable mapping instead of auto-generated variables |
| Cargo.toml | Updates dependencies to use external repositories for pest_consume and mcrl2-sys |
| .gitmodules | Removes submodules for mCRL2, boost, and cpptrace (moved to mcrl2-sys repo) |
| 3rd-party/* | Removes vendored pest_consume and mCRL2-related code |
| tools/mcrl2/* | Removes mcrl2-sys crate (moved to separate repository) |
mlaveaux
force-pushed
the
feature/symbolic_lts_bdd
branch
from
3f5ff5a to
bd1aa0d
Compare
…mand to merc-sym.
Also take cases where there are fixpoint but it is not the first one, such as "<true> nu X ..."
…different levels of the partition and the signature. This was unclear from the pseudocode.
…wice as slow with linking as thin LTO. This is 5 minutes in total on a full rebuild for the GUI tools, and is now 2,5 minutes.
* It seems that rusty file dialog has been rewritten to drop about 200 dependencies, so that is nice.
… the miri feature.
…temporary strings
…o clean works as expected.
…gref implementation. * The implementation makes no sense, but it does compute the right answer, whereas, the implementation that made sense did not.
mlaveaux
force-pushed
the
feature/symbolic_lts_bdd
branch
from
87df6b7 to
313677a
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Also started with the signature based strong symbolic bisimulation. This is not yet working correctly, and the quotient is also missing.